FDL - Step of Proof: nat_well_founded

Step of Proof: nat_well_founded

Inference at * 1
Iof proof for Lemma nat well founded:

P:(

). (

j:

. (

k:

. (k < j)

P(k))

P(j))

{

n:

. P(n)}

by ((RepD)

CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n

C)) (first_tok :t) inil_term)))

C1:

C1: 1. P :

C1: 2.

j:

. (

k:

. (k < j)

P(k))

P(j)

C1:

n:

. P(n)

C.

Definitions t T, {T}, x(s), P Q, , x:A. B(x),

Lemmas nat wf